PZ86 Mutual Exclusion

PZ86 Mutual Exclusion

This example is based on Pnueli and Zuck's work about the n-process mutual exclusion problem. Mutual exclusion problem means that there are n processes in a system; however, at each time, at most one process could take control of the critical section. In the following we model this problem in PCSP and use it to check some properties; what is more, we define a safety specification and then use refinement checking to verify if this model satisfies the safety requirement.

First of all, we need to declare how many processes we want in our model and define some global variables to record how many processes are in the same state at the same time.

#define N 2;
var EnterCounter;
var HighCounter;
var LowCounter;
var TieCounter;
var AdmitCounter;
var CriticalSectionCounter; // used to record how many processes are in critical section at the same time; should be 0 or 1 all the time.

The following is the system model.

Process0 = tau -> Process0 [] tau{EnterCounter++;} -> Process2;
Process2 = [(!(HighCounter>0||LowCounter>0||TieCounter>0)) || AdmitCounter>0] tau -> Process3;
Process3 = tau{EnterCounter--; HighCounter++;} -> Process4 [] tau{EnterCounter--; LowCounter++} -> Process7;
Process4 = [HighCounter>1||AdmitCounter>0] tau -> Process5 [] [!(HighCounter>1||AdmitCounter>0)] enterCS {CriticalSectionCounter++;} -> Process10;
Process5 = tau{TieCounter++; HighCounter--;} -> Process6;
Process6 = [!(HighCounter>0||AdmitCounter>0)] tau -> Process9;
Process7 = [!(HighCounter>0||TieCounter>0||AdmitCounter>0)] tau -> Process8;
Process8 = tau{LowCounter--; TieCounter++;} -> Process9;
Process10 = [!(LowCounter>0||HighCounter>1||TieCounter>0)] tau -> Process12 [] [(LowCounter>0||HighCounter>1||TieCounter>0)] tau -> Process11;
Process11 = exitCS{HighCounter--; CriticalSectionCounter--;} -> Process0;
Process12 = tau{AdmitCounter++; HighCounter--;} -> Process13;
Process13 = [EnterCounter==0] tau -> Process14;
Process14 = exitCS{AdmitCounter--; CriticalSectionCounter--;} -> Process0;
Process9 = pcase{
[0.5] : tau{TieCounter--; HighCounter++;} -> Process4
default : tau{TieCounter--; LowCounter++;} -> Process7
};
System = ||| {N} @ (Process0);

These processes represent all the situations a process could get into; System means there are N processes in the system now. In order to check if this system is always "safe", we define the following process to indicate at most one process could enter critical section.

Spec = enterCS -> exitCS -> Spec;
#assert System refines aSpec with pmax;

Spec means that after every enterCS event, there should be a exitCS following. This could prevent the system from having two or more enterCS happen successively. Then we could check the probability that System could refine Spec and the result indicates the reliablity of this system.

Some properties that can be checked are the following:

#assert System deadlockfree;

#define all_high (HighCounter==N);
#assert System |= <>all_high && <>all_low with pmax;